perm filename DOC[EKL,SYS] blob sn#860108 filedate 1988-08-18 generic text, type C, neo UTF8
COMMENT ⊗   VALID 00008 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Facts about reverse:
C00004 00003	A proof of Ramsey's Theorem
C00005 00004	The pigeon hole principle and proofs that permutations are a group
C00009 00005	general facts about maps in the category of sets
C00012 00006	A problem in non monotonic reasoning
C00013 00007	The quantifier `there exists exactly one'
C00014 00008	The Landau project
C00016 ENDMK
C⊗;
;Facts about reverse:

;File names:

;natnum[ekl,sys]                ;facts of natural numbers, involving <,',+ and *

;lispax[ekl,sys]                ;axioms of LISP

;reverse[ekl,sys]               ;facts about reverse

;lthrev[ekl,sys]                ;facts about length and reverse

;Facts about reverse are given in the following order

;                lispax
;                   |    
;                   ↓                 
;                reverse           natnum
;                   |                 |
;                   |_________________|
;                            |                                       
;                            ↓
;                          lthrev
;A proof of Ramsey's Theorem

;File names:

;natnum[ekl,sys]                ;facts of natural numbers, involving <,',+ and *

;natset[ekl,sys]                ;facts of set theory

;ramsey[ekl,sys]                ;proof of the theorem

;File organization:

;               natnum    
;                  ↓
;               natset
;                  ↓
;               ramsey

;The functional interpretation of Infinite Ramsey
;This is a fragment, i.e. the base case in the main induction.

;               ramsey.nci
;The pigeon hole principle and proofs that permutations are a group
;(see the paper G.Bellin and J.Ketonen, Experiments in Authomatic Theorem Proving)
;which explains the material.

;File names:

;normal[ekl,sys]                ;a normalizer of (propositional) expressions

;natnum[ekl,sys]                ;facts of natural numbers, involving <,',+ and *

;minus[ekl,sys]                 ;facts of natural numbers, involving ≤ and -

;lispax[ekl,sys]                ;axioms of LISP

;allp[ekl,sys]                  ;facts about the bounded quantifier allp

;set[ekl,sys]                   ;rudiments of set theory

;length[ekl,sys]                ;length of lists

;nth[ekl,sys]                   ;the nth function and its relatives

;appl[ekl,sys]                  ;two notions of application, via lists of numbers

;sums[ekl,sys]                  ;finite sums and unions

;mult[ekl,sys]                  ;multiplicity and their properties

;pigeon[ekl,sys]                ;the prigeon hole principle in 2nd order arithmetic

;alpig[ekl,sys]                 ;application of the pigeon hole to alists

;invima[ekl,sys];               ;a generalization (third application)

;assoc[ekl,sys]                 ;permutations are a group (using alists)

;lpig[ekl,sys]                  ;application of the pigeon hole to lists of numbers

;permp[ekl,sys]                 ;permutations are a group (lists, using predicates)

;permf[ekl,sys]                 ;permutations are a group (lists, using functions)

;File organization:

;      natnum        normal              lispax
;         |            |                    ↓
;         |____________|                   allp   ;fix somepfacts
;               ↓                           ↓
;             minus                        set
;               |___________________________|
;                            ↓
;                          length
;                            ↓
;                           nth 
;                            ↓
;                           appl
;               _____________|______________________
;               ↓            ↓         ↓           ↓
;	       sums        assoc     permp        permf
;               ↓
;              mult
;               ↓
;             pigeon
;         _____________
;         ↓           ↓ 
;       alpig       lpig
;         ↓
;      invima 
 
;general facts about maps in the category of sets

;catset.gen[ekl,sys]
;A problem in non monotonic reasoning

;bird[ekl,sys]                  ;most birds can fly, but not all: 
;                               ;use of the predicate `ab' (abnormal)  
;The quantifier `there exists exactly one'

;unique[ekl,sys]                ;∃!
;The Landau project

;formalizing ``Foundations of Analysis'' by E.Landau, Chelsea NY 1951

;the following files contain the formalization of the first 50 pages 

;nat.lan[ekl,sys]                             ;natural numbers

;frac.lan[ekl,sys]                            ;fractions

;rat.lan[ekl,sys]                             ;rational numbers

;cut.lan[ekl,sys]                             ;Dedekind cuts

;File organization:

;         nat.lan                lispax[ekl,sys]
;            |                         |
;            |_________________________|
;                         |
;                         ↓
;                      frac.lan
;                         |
;                         ↓
;                      rat.lan
;                         |
;                         ↓
;                      cut.lan